f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
↳ QTRS
↳ DependencyPairsProof
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
F'(s(x), y, y) → F'(y, x, s(x))
F(g(x)) → F(x)
F(g(x)) → F(f(x))
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
F'(s(x), y, y) → F'(y, x, s(x))
F(g(x)) → F(x)
F(g(x)) → F(f(x))
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
F'(s(x), y, y) → F'(y, x, s(x))
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F'(s(x), y, y) → F'(y, x, s(x))
The value of delta used in the strict ordering is 9.
POL(F'(x1, x2, x3)) = (4)x_1 + (4)x_2 + x_3
POL(s(x1)) = 3 + (4)x_1
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
↳ QDP
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
F(g(x)) → F(f(x))
F(g(x)) → F(x)
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))
The following pairs can be oriented strictly and are deleted.
The remaining pairs can at least be oriented weakly.
F(g(x)) → F(f(x))
F(g(x)) → F(x)
The value of delta used in the strict ordering is 1.
POL(f(x1)) = x_1
POL(g(x1)) = 4 + (4)x_1
POL(h(x1)) = 1/2
POL(F(x1)) = (1/4)x_1
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
↳ QTRS
↳ DependencyPairsProof
↳ QDP
↳ DependencyGraphProof
↳ AND
↳ QDP
↳ QDP
↳ QDPOrderProof
↳ QDP
↳ PisEmptyProof
f(g(x)) → g(f(f(x)))
f(h(x)) → h(g(x))
f'(s(x), y, y) → f'(y, x, s(x))